m, a, a', b, b':. (a = a' mod m)  (b = b' mod m)  ((a = b mod m)  (a' = b' mod m)) 

latex

Definitions	P  Q, P & Q, P  Q, P  Q, a = b mod m, x:A. B(x), t  T
Lemmas	eqmod transitivity, eqmod inversion, eqmod wf